filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))
↳ QTRS
↳ DependencyPairsProof
filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))
SIEVE(cons(s(N), Y)) → FILTER(Y, N, N)
FILTER(cons(X, Y), 0, M) → FILTER(Y, M, M)
NATS(N) → NATS(s(N))
ZPRIMES → SIEVE(nats(s(s(0))))
ZPRIMES → NATS(s(s(0)))
SIEVE(cons(0, Y)) → SIEVE(Y)
FILTER(cons(X, Y), s(N), M) → FILTER(Y, N, M)
SIEVE(cons(s(N), Y)) → SIEVE(filter(Y, N, N))
filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
SIEVE(cons(s(N), Y)) → FILTER(Y, N, N)
FILTER(cons(X, Y), 0, M) → FILTER(Y, M, M)
NATS(N) → NATS(s(N))
ZPRIMES → SIEVE(nats(s(s(0))))
ZPRIMES → NATS(s(s(0)))
SIEVE(cons(0, Y)) → SIEVE(Y)
FILTER(cons(X, Y), s(N), M) → FILTER(Y, N, M)
SIEVE(cons(s(N), Y)) → SIEVE(filter(Y, N, N))
filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
NATS(N) → NATS(s(N))
filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
FILTER(cons(X, Y), 0, M) → FILTER(Y, M, M)
FILTER(cons(X, Y), s(N), M) → FILTER(Y, N, M)
filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FILTER(cons(X, Y), 0, M) → FILTER(Y, M, M)
FILTER(cons(X, Y), s(N), M) → FILTER(Y, N, M)
The value of delta used in the strict ordering is 4.
POL(FILTER(x1, x2, x3)) = (4)x_1
POL(cons(x1, x2)) = 1 + (4)x_2
POL(s(x1)) = 0
POL(0) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
SIEVE(cons(0, Y)) → SIEVE(Y)
SIEVE(cons(s(N), Y)) → SIEVE(filter(Y, N, N))
filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SIEVE(cons(0, Y)) → SIEVE(Y)
SIEVE(cons(s(N), Y)) → SIEVE(filter(Y, N, N))
The value of delta used in the strict ordering is 1/16.
POL(SIEVE(x1)) = (1/4)x_1
POL(cons(x1, x2)) = 1/4 + (1/4)x_1 + (4)x_2
POL(filter(x1, x2, x3)) = (4)x_1
POL(s(x1)) = (1/4)x_1
POL(0) = 1/4
filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))
filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))
sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))
zprimes → sieve(nats(s(s(0))))